es:ES, i:Id, k:Knd. kindtype(i;k)  Type 

latex

Definitions	x:A. B(x), t  T, kindtype(i;k), if b t else f fi, es-M(es), es-V(es), 1of(t), 2of(t), P  Q, true, false, Prop, ES, Unit, P & Q, , P  Q, P  Q,
Lemmas	isrcv wf, bool wf, eqtt to assert, lnk wf, tagof wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, actof wf, Knd wf, Id wf, event system wf, islocal-not-isrcv